FDL - Step of Proof: before

Step of Proof: before_last

11,40

Inference at * 2 1 4
Iof proof for Lemma before last:

1. T : Type
2. T List
3. u : T
4. v : T List
5.

x:T. (x

(

(x = last(v)))

x before last(v)

v
6. x : T
7. (x

v)
8.

(x = last([u / v]))

[x; last(v)]

by ((((Fold `l_before` 0)

CollapseTHEN (BackThruSomeHyp))

)

CollapseTHEN (

C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n)) (first_tok :t) inil_term)))

C1:

(x = last(v))

Definitions t T, P Q, x:A. B(x), x before y l